ds:x:Id fp Type, da:k:Knd fp Type, k:Knd, x:Id, n:, f:(State(ds)Valtype(da;k)ds(x)?Void).
update-spec1(k;x;n;s,v.f(s,v))  update-spec(ds;da) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, , Void, IdDeq, x.A(x), f(x)?z, Top, KindDeq, x:AB(x), State(ds), <a,b>, 2of(t), 1of(t), x:AB(x), type List, nil, f(a), x(s1,s2), car.cdr, x : v, Valtype(da;k), update-spec1(k;x;n;s,v.f(s;v)), update-spec(ds;da)
Lemmas	fpf-single wf, pi1 wf, pi2 wf, decl-state wf, Kind-deq wf, top wf, fpf-cap wf, id-deq wf, nat wf, Knd wf, fpf wf, Id wf